| Definitions | x:A  B(x),  , a < b, s = t, A c B,  x:A. B(x), (x  l), prop{i:l}, t T,  x:A. B(x), fpf(A; a.B(a)), rec(x.A(x)), ecl(ds; da), {x:A| B(x)} , type List, f(a), False,  A, P   Q, ecl-ex(x), guard(T), P  Q, left + right, decidable(P),  , Type, x:A  B(x), P  Q, P Q, P Q, s-insert(x; l),  , A  B, iseg(T; l1; l2), merge(as; bs), void, #$n, subtype(S; T), <a, b>,  b,  , Unit, if b then t else f fi , True,  T, (i = j),  b, l_all(L; T; x.P(x)), star-append(T; P; Q), ecl ind eclcatch compseq tag def, ecl ind eclthrow compseq tag def, ecl ind eclact compseq tag def, ecl ind eclrepeat compseq tag def, ecl ind eclor compseq tag def, ecl ind ecland compseq tag def, ecl ind eclseq compseq tag def, ecl ind eclbase compseq tag def, ecl-halt(ds; da; x), event-info(ds;da), eclcatch(a; l), eclthrow(a; n), eclact(a; n), cons(car; cdr), eclrepeat(a), eclor(a; b), ecland(a; b), eclseq(a; b), ma-valtype(da; k), decl-state(ds), eclbase(k; test), Knd,  x.A(x),  x. t(x), Id, sq_type(T) |